﻿#include <iostream>
#include <fstream>
#include <vector>
#include <chrono>
#include <sstream>
#include <unordered_map>
#include <unordered_set>
#include <stack>
#include <queue>
using namespace std;
using namespace chrono;
struct Node {
    int var;
    bool negated;
    Node() : var(0), negated(false) {}
    Node(int v, bool n) : var(v), negated(n) {}
};
struct CNFFormula {
    int numVars;
    vector<vector<Node>> clauses;
    vector<vector<int>*> positiveLiteralToClauses;
    vector<vector<int>*> negativeLiteralToClauses;
    vector<unordered_set<int>> clauseToLiterals;    // 子句到字面量的映射

    CNFFormula(int nVars) : numVars(nVars) {
        positiveLiteralToClauses.resize(numVars + 1);
        negativeLiteralToClauses.resize(numVars + 1);
    }

    void addClause(const vector<Node>& clause) {
        int clauseIndex = clauses.size();
        clauses.push_back(clause);
        unordered_set<int> literals;

        for (const auto& node : clause) {
            int literal = node.var * (node.negated ? 1 : -1);
            literals.insert(literal);
            if (literal > 0) {
                if (!positiveLiteralToClauses[literal]) {
                    positiveLiteralToClauses[literal] = new vector<int>();
                }
                positiveLiteralToClauses[literal]->push_back(clauseIndex);
            }
            else {
                int var = -literal;
                if (!negativeLiteralToClauses[var]) {
                    negativeLiteralToClauses[var] = new vector<int>();
                }
                negativeLiteralToClauses[var]->push_back(clauseIndex);
            }
        }
        clauseToLiterals.push_back(literals);
    }

    void removeClause(int clauseIndex) {
        if (clauseIndex >= clauseToLiterals.size()) return;

        for (int literal : clauseToLiterals[clauseIndex]) {
            if (literal > 0 && positiveLiteralToClauses[literal]) {
                auto& clauses = *positiveLiteralToClauses[literal];
                clauses.erase(remove(clauses.begin(), clauses.end(), clauseIndex), clauses.end());
            }
            else if (literal < 0 && negativeLiteralToClauses[-literal]) {
                auto& clauses = *negativeLiteralToClauses[-literal];
                clauses.erase(remove(clauses.begin(), clauses.end(), clauseIndex), clauses.end());
            }
        }
        clauseToLiterals[clauseIndex].clear();
    }

    const vector<int>& getClausesWithLiteral(int literal) const {
        if (literal > 0) {
            return *positiveLiteralToClauses[literal];
        }
        else {
            return *negativeLiteralToClauses[-literal];
        }
    }
};


milliseconds totalFindingTime(0);

CNFFormula readCNF(const string& filename) {
    ifstream file(filename);
    CNFFormula cnf(0);
    string line;
    int numVars = 0;

    while (getline(file, line)) {
        if (line.empty() || line[0] == 'c') continue;
        else if (line[0] == 'p') {
            istringstream iss(line);
            string dummy;
            int numClauses;
            iss >> dummy >> dummy >> numVars >> numClauses;
            cnf = CNFFormula(numVars);
        }
        else {
            istringstream ss(line);
            int var;
            vector<Node> clause;
            while (ss >> var && var != 0) {
                clause.push_back(Node(abs(var), var > 0));
            }
            cnf.addClause(clause);
        }
    }

    return cnf;
}

bool isSatisfied(const CNFFormula& cnf, const vector<int>& assignment) {
    for (const auto& clause : cnf.clauses) {
        bool clauseSatisfied = false;
        for (const auto& node : clause) {
            if (assignment[node.var - 1] != -1) {
                bool value = assignment[node.var - 1];
                if (!node.negated) value = !value;
                if (value) {
                    clauseSatisfied = true;
                    break;
                }
            }
        }
        if (!clauseSatisfied) {
            return false;
        }
    }
    return true;
}

void pureLiteralElimination(CNFFormula& cnf, vector<int>& assignment, vector<bool>& clauseDeleted, vector<int>& pureLiterals) {
    vector<int> literalCount(cnf.numVars + 1, 0);
    vector<bool> isPureLiteral(cnf.numVars + 1, true);
    for (const auto& clause : cnf.clauses) {
        for (const auto& node : clause) {
            int literal = node.var * (node.negated ? 1 : -1);
            literalCount[abs(literal)]++;
            int oppositeLiteral = -literal;
            const vector<int>& oppositeClauses = cnf.getClausesWithLiteral(oppositeLiteral);
            if (&oppositeClauses != nullptr) {
                isPureLiteral[abs(literal)] = false;
            }
            else {
            }
        }
    }
    unordered_set<int> clausesToRemove;
    for (int var = 1; var <= cnf.numVars; ++var) {
        if (isPureLiteral[var] && assignment[var - 1] == -1) {
            if (cnf.positiveLiteralToClauses[var] && !cnf.positiveLiteralToClauses[var]->empty()) {
                assignment[var - 1] = 1;
                pureLiterals.push_back(var);
            }
            else if (cnf.negativeLiteralToClauses[var] && !cnf.negativeLiteralToClauses[var]->empty()) {
                assignment[var - 1] = 0;
                pureLiterals.push_back(-var);
            }
            if (assignment[var - 1] == 1 && cnf.positiveLiteralToClauses[var]) {
                for (int clauseIndex : *cnf.positiveLiteralToClauses[var]) {
                    clauseDeleted[clauseIndex] = true;
                    clausesToRemove.insert(clauseIndex);
                }
            }
            else if (assignment[var - 1] == 0 && cnf.negativeLiteralToClauses[var]) {
                for (int clauseIndex : *cnf.negativeLiteralToClauses[var]) {
                    clauseDeleted[clauseIndex] = true;
                    clausesToRemove.insert(clauseIndex);
                }
            }
        }
    }
    for (int clauseIndex : clausesToRemove) {
        cnf.removeClause(clauseIndex);
    }
}



bool propagateLiteral(int literal, CNFFormula& cnf, vector<int>& assignment,
    vector<int>& clauseChangeLog, vector<bool>& clauseDeleted,
    vector<int>& unassignedCount, vector<Node>& lastUnassignedNode) {
    int var = abs(literal);
    bool value = literal > 0;
    if (assignment[var - 1] != -1) return true;

    assignment[var - 1] = value ? 1 : 0;

    const auto& relatedClauses1 = cnf.getClausesWithLiteral(literal);
    for (int clauseIndex : relatedClauses1) {
        if (clauseDeleted[clauseIndex]) continue;
        clauseDeleted[clauseIndex] = true;
        clauseChangeLog.push_back(clauseIndex);
    }

    try {
        const auto& relatedClauses2 = cnf.getClausesWithLiteral(-literal);
    }
    catch (...) {
        return true;
    }
    const auto& relatedClauses2 = cnf.getClausesWithLiteral(-literal);
    if (&relatedClauses2 == nullptr) {
        return true;
    }
    for (int clauseIndex : relatedClauses2) {
        if (clauseDeleted[clauseIndex]) continue;
        unassignedCount[clauseIndex] = 0;
        for (const auto& node : cnf.clauses[clauseIndex]) {
            int assignedValue = assignment[node.var - 1];
            if (assignedValue == (node.negated ? 1 : 0)) {
                clauseDeleted[clauseIndex] = true;
                clauseChangeLog.push_back(clauseIndex);
                break;
            }
            if (assignedValue == -1) {
                unassignedCount[clauseIndex]++;
                lastUnassignedNode[clauseIndex] = node;
            }
        }

        if (unassignedCount[clauseIndex] == 0 && !clauseDeleted[clauseIndex]) {
            return false; // 发现冲突，终止传播
        }

        if (unassignedCount[clauseIndex] == 1 && !clauseDeleted[clauseIndex]) {
            int newLiteral = lastUnassignedNode[clauseIndex].var * (lastUnassignedNode[clauseIndex].negated ? 1 : -1);
            if (!propagateLiteral(newLiteral, cnf, assignment, clauseChangeLog, clauseDeleted, unassignedCount, lastUnassignedNode)) {
                return false;
            }
        }
    }
    return true;
}

bool unitPropagation(CNFFormula& cnf, vector<int>& assignment,
    vector<int>& clauseChangeLog, vector<bool>& clauseDeleted) {
    vector<int> unassignedCount(cnf.clauses.size(), 0);
    vector<Node> lastUnassignedNode(cnf.clauses.size());
    for (int i = 0; i < cnf.clauses.size(); ++i) {
        if (clauseDeleted[i]) continue;
        int count = 0;
        for (const auto& node : cnf.clauses[i]) {
            int assignedValue = assignment[node.var - 1];
            if (assignedValue == -1) {
                count++;
                lastUnassignedNode[i] = node;
            }
            else if (assignedValue == (node.negated ? 1 : 0)) {
                clauseDeleted[i] = true;
                clauseChangeLog.push_back(i);
                break;
            }
        }
        unassignedCount[i] = count;
        if (count == 1 && !clauseDeleted[i]) {
            int literal = lastUnassignedNode[i].var * (lastUnassignedNode[i].negated ? 1 : -1);
            if (!propagateLiteral(literal, cnf, assignment, clauseChangeLog, clauseDeleted, unassignedCount, lastUnassignedNode)) {
                return false;
            }
        }
    }
    return true;
}
int selectVariableMOMS(const CNFFormula& cnf, const vector<int>& assignment, vector<bool>& clauseDeleted) {
    vector<int> negCount(cnf.numVars, 0);
    vector<int> posCount(cnf.numVars, 0);
    int minClauseSize = INT_MAX;

    // 找到最短的子句长度
    for (int i = 0; i < cnf.clauses.size(); ++i) {
        if (clauseDeleted[i]) continue;
        const auto& clause = cnf.clauses[i];
        if (clause.size() < minClauseSize) {
            minClauseSize = clause.size();
        }
    }

    // 统计最短子句中变量的出现次数
    for (int i = 0; i < cnf.clauses.size(); ++i) {
        if (clauseDeleted[i] || cnf.clauses[i].size() != minClauseSize) continue;
        const auto& clause = cnf.clauses[i];
        for (const auto& node : clause) {
            if (assignment[node.var - 1] == -1) {
                if (node.negated) {
                    negCount[node.var - 1]++;
                }
                else {
                    posCount[node.var - 1]++;
                }
            }
        }
    }
    int bestVar = -1;
    int bestScore = 0;
    int bestSign = 1;
    for (int i = 0; i < cnf.numVars; ++i) {
        if (assignment[i] == -1) {
            int score = posCount[i] + negCount[i];
            if (score > bestScore) {
                bestScore = score;
                bestVar = i + 1;
                bestSign = (posCount[i] >= negCount[i]) ? 1 : -1;
            }
        }
    }

    if (bestVar == -1) {
        return 0;
    }

    return bestVar * bestSign;
}



bool dpllIterative(CNFFormula& cnf, vector<int>& assignment) {
    stack<vector<pair<int, int>>> stateStack;
    vector<pair<int, int>> trail;
    vector<bool> clauseDeleted(cnf.clauses.size(), false);
    stack<vector<int>> changeLogStack;
    vector<int> clauseChangeLog;
    vector<int> pureLiterals;
    changeLogStack.push(clauseChangeLog);
    stateStack.push(trail);
    pureLiteralElimination(cnf, assignment, clauseDeleted, pureLiterals);
    while (!stateStack.empty()) {
        trail = stateStack.top();
        stateStack.pop();
        fill(assignment.begin(), assignment.end(), -1);
        for (const int a : pureLiterals) {
            if (a < 0) {
                assignment[abs(a) - 1] = 0;
            }
            else {
                assignment[abs(a) - 1] = 1;
            }

        }
        for (const pair<int, int>& p : trail) {
            int index = p.first;
            int value = p.second;
            assignment[index] = value;
        }
        if (!changeLogStack.empty()) {
            auto changes = changeLogStack.top();
            changeLogStack.pop();
            for (int clauseIndex : changes) {
                clauseDeleted[clauseIndex] = false;
            }
        }
        bool result = unitPropagation(cnf, assignment, clauseChangeLog, clauseDeleted);
        bool fin_result = isSatisfied(cnf, assignment);
        if (fin_result) {
            return true;
        }
        changeLogStack.push(clauseChangeLog);
        clauseChangeLog.clear();
        if (!stateStack.empty() && !result) {
            continue;
        }

        int literal = selectVariableMOMS(cnf, assignment, clauseDeleted);
        if (literal == 0) {
            continue;
        }
        int var = abs(literal);
        bool preferNegated = literal < 0;  // 是否优先尝试负变元

        trail.push_back({ var - 1, preferNegated ? 1 : 0 });
        stateStack.push(trail);
        trail.back().second = preferNegated ? 0 : 1;
        stateStack.push(trail);
    }
    return false;
}


int main() {
    CNFFormula cnf = readCNF("D:/Desktop/SAT测试备选算例/Beijing/enddr2-10-by-5-1.cnf");
    // CNFFormula cnf = readCNF("D:/Desktop/SAT测试备选算例/满足算例/S/problem9-100.cnf");
    auto start = high_resolution_clock::now();
    vector<int> assignment(cnf.numVars, -1);
    bool result = dpllIterative(cnf, assignment);
    auto stop = high_resolution_clock::now();
    auto duration = duration_cast<milliseconds>(stop - start);

    if (result) {
        cout << "问题有解" << endl;
        for (int i = 0; i < cnf.numVars; ++i) {
            //可真可假
            if (assignment[i] == -1) {
                assignment[i] = 1;
            }
            cout << "变元 " << i + 1 << " 的赋值为: " << (assignment[i]) << endl;
        }
    }
    else {
        cout << "问题无解" << endl;
    }
    cout << "算法运行时间: " << duration.count() / 1000.0 << " 秒" << endl;
    return 0;
}